\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{ArithExp} : \coqdockw{Set} := \coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_exp\_num}   : \coqdocvar{Integer}  \ensuremath{\rightarrow} \coqdocvar{ArithExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_exp\_id}    : \coqdocvar{Id}       \ensuremath{\rightarrow} \coqdocvar{ArithExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_exp\_plus}  : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_exp\_minus} : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_exp\_mult}  : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_exp\_div}   : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{arith\_exp\_mod}   : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp}\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}
